IdrisDoc: [builtins]

[builtins]

(~=~) : (x : a) -> (y : b) -> Type

Explicit heterogeneous ("John Major") equality. Use this when Idris
incorrectly chooses homogeneous equality for (=).

Fixity
Non-associative, precedence 5
b

the type of the right side

a

the type of the left side

x

the left side

y

the right side

world : World -> prim__WorldType
void : Void -> a

The eliminator for the Void type.

unsafePerformPrimIO : PrimIO a -> a
unsafePerformIO : IO' ffi a -> a
trans : (a = b) -> (b = c) -> a = c

Transitivity of propositional equality

sym : (left = right) -> right = left

Symmetry of propositional equality

run__provider : IO a -> PrimIO a
run__IO : IO' ffi () -> PrimIO ()
rewrite__impl : (P : a -> Type) -> (x = y) -> P y -> P x

Perform substitution in a term according to some equality.

Like replace, but with an explicit predicate, and applying the rewrite
in the other direction, which puts it in a form usable by the rewrite
tactic and term.

replace : (x = y) -> P x -> P y

Perform substitution in a term according to some equality.

really_believe_me : a -> b

Subvert the type checker. This function will reduce in the type checker.
Use it with extreme care - it can result in segfaults or worse!

prim_write : String -> IO' l Int
prim_read : IO' l String
prim_pokeSingle : Ptr -> Int -> Double -> IO Int

Single precision floats are marshalled to Doubles

prim_pokePtr : Ptr -> Int -> Ptr -> IO Int
prim_pokeDouble : Ptr -> Int -> Double -> IO Int
prim_poke8 : Ptr -> Int -> Bits8 -> IO Int
prim_poke64 : Ptr -> Int -> Bits64 -> IO Int
prim_poke32 : Ptr -> Int -> Bits32 -> IO Int
prim_poke16 : Ptr -> Int -> Bits16 -> IO Int
prim_peekSingle : Ptr -> Int -> IO Double

Single precision floats are marshalled to Doubles

prim_peekPtr : Ptr -> Int -> IO Ptr
prim_peekDouble : Ptr -> Int -> IO Double
prim_peek8 : Ptr -> Int -> IO Bits8
prim_peek64 : Ptr -> Int -> IO Bits64
prim_peek32 : Ptr -> Int -> IO Bits32
prim_peek16 : Ptr -> Int -> IO Bits16
prim_lenString : String -> Int
prim_io_pure : a -> PrimIO a
prim_io_bind : PrimIO a -> (a -> PrimIO b) -> PrimIO b
prim_fwrite : Ptr -> String -> IO' l Int
prim_fread : Ptr -> IO' l String
prim_fork : PrimIO () -> PrimIO Ptr
prim__zextInt_BigInt : Int -> Integer
prim__zextInt_B64 : Int -> Bits64
prim__zextInt_B32 : Int -> Bits32
prim__zextInt_B16 : Int -> Bits16
prim__zextChar_BigInt : Char -> Integer
prim__zextB8_Int : Bits8 -> Int
prim__zextB8_BigInt : Bits8 -> Integer
prim__zextB8_B64 : Bits8 -> Bits64
prim__zextB8_B32 : Bits8 -> Bits32
prim__zextB8_B16 : Bits8 -> Bits16
prim__zextB64_BigInt : Bits64 -> Integer
prim__zextB32_Int : Bits32 -> Int
prim__zextB32_BigInt : Bits32 -> Integer
prim__zextB32_B64 : Bits32 -> Bits64
prim__zextB16_Int : Bits16 -> Int
prim__zextB16_BigInt : Bits16 -> Integer
prim__zextB16_B64 : Bits16 -> Bits64
prim__zextB16_B32 : Bits16 -> Bits32
prim__xorInt : Int -> Int -> Int
prim__xorChar : Char -> Char -> Char
prim__xorBigInt : Integer -> Integer -> Integer
prim__xorB8 : Bits8 -> Bits8 -> Bits8
prim__xorB64 : Bits64 -> Bits64 -> Bits64
prim__xorB32 : Bits32 -> Bits32 -> Bits32
prim__xorB16 : Bits16 -> Bits16 -> Bits16
prim__writeString : prim__WorldType -> String -> Int
prim__writeFile : prim__WorldType -> Ptr -> String -> Int
prim__vm : prim__WorldType -> Ptr
prim__uremInt : Int -> Int -> Int
prim__uremChar : Char -> Char -> Char
prim__uremBigInt : Integer -> Integer -> Integer
prim__uremB8 : Bits8 -> Bits8 -> Bits8
prim__uremB64 : Bits64 -> Bits64 -> Bits64
prim__uremB32 : Bits32 -> Bits32 -> Bits32
prim__uremB16 : Bits16 -> Bits16 -> Bits16
prim__udivInt : Int -> Int -> Int
prim__udivChar : Char -> Char -> Char
prim__udivBigInt : Integer -> Integer -> Integer
prim__udivB8 : Bits8 -> Bits8 -> Bits8
prim__udivB64 : Bits64 -> Bits64 -> Bits64
prim__udivB32 : Bits32 -> Bits32 -> Bits32
prim__udivB16 : Bits16 -> Bits16 -> Bits16
prim__truncInt_B8 : Int -> Bits8
prim__truncInt_B64 : Int -> Bits64
prim__truncInt_B32 : Int -> Bits32
prim__truncInt_B16 : Int -> Bits16
prim__truncBigInt_Int : Integer -> Int
prim__truncBigInt_Char : Integer -> Char
prim__truncBigInt_B8 : Integer -> Bits8
prim__truncBigInt_B64 : Integer -> Bits64
prim__truncBigInt_B32 : Integer -> Bits32
prim__truncBigInt_B16 : Integer -> Bits16
prim__truncB64_Int : Bits64 -> Int
prim__truncB64_B8 : Bits64 -> Bits8
prim__truncB64_B32 : Bits64 -> Bits32
prim__truncB64_B16 : Bits64 -> Bits16
prim__truncB32_Int : Bits32 -> Int
prim__truncB32_B8 : Bits32 -> Bits8
prim__truncB32_B16 : Bits32 -> Bits16
prim__truncB16_Int : Bits16 -> Int
prim__truncB16_B8 : Bits16 -> Bits8
prim__toStrInt : Int -> String
prim__toStrChar : Char -> String
prim__toStrBigInt : Integer -> String
prim__toStrB8 : Bits8 -> String
prim__toStrB64 : Bits64 -> String
prim__toStrB32 : Bits32 -> String
prim__toStrB16 : Bits16 -> String
prim__toFloatInt : Int -> Double
prim__toFloatChar : Char -> Double
prim__toFloatBigInt : Integer -> Double
prim__toFloatB8 : Bits8 -> Double
prim__toFloatB64 : Bits64 -> Double
prim__toFloatB32 : Bits32 -> Double
prim__toFloatB16 : Bits16 -> Double
prim__systemInfo : Int -> String
prim__syntactic_eq : (a : Type) -> (b : Type) -> (x : a) -> (y : b) -> Maybe (x = y)
prim__subInt : Int -> Int -> Int
prim__subFloat : Double -> Double -> Double
prim__subChar : Char -> Char -> Char
prim__subBigInt : Integer -> Integer -> Integer
prim__subB8 : Bits8 -> Bits8 -> Bits8
prim__subB64 : Bits64 -> Bits64 -> Bits64
prim__subB32 : Bits32 -> Bits32 -> Bits32
prim__subB16 : Bits16 -> Bits16 -> Bits16
prim__strToFloat : String -> Double
prim__strTail : String -> String
prim__strSubstr : Int -> Int -> String -> String
prim__strRev : String -> String
prim__strIndex : String -> Int -> Char
prim__strHead : String -> Char
prim__strCons : Char -> String -> String
prim__stdout : Ptr
prim__stdin : Ptr
prim__stderr : Ptr
prim__sremInt : Int -> Int -> Int
prim__sremChar : Char -> Char -> Char
prim__sremBigInt : Integer -> Integer -> Integer
prim__sremB8 : Bits8 -> Bits8 -> Bits8
prim__sremB64 : Bits64 -> Bits64 -> Bits64
prim__sremB32 : Bits32 -> Bits32 -> Bits32
prim__sremB16 : Bits16 -> Bits16 -> Bits16
prim__slteInt : Int -> Int -> Int
prim__slteFloat : Double -> Double -> Int
prim__slteChar : Char -> Char -> Int
prim__slteBigInt : Integer -> Integer -> Int
prim__slteB8 : Bits8 -> Bits8 -> Int
prim__slteB64 : Bits64 -> Bits64 -> Int
prim__slteB32 : Bits32 -> Bits32 -> Int
prim__slteB16 : Bits16 -> Bits16 -> Int
prim__sltInt : Int -> Int -> Int
prim__sltFloat : Double -> Double -> Int
prim__sltChar : Char -> Char -> Int
prim__sltBigInt : Integer -> Integer -> Int
prim__sltB8 : Bits8 -> Bits8 -> Int
prim__sltB64 : Bits64 -> Bits64 -> Int
prim__sltB32 : Bits32 -> Bits32 -> Int
prim__sltB16 : Bits16 -> Bits16 -> Int
prim__sizeofPtr : Int
prim__shlInt : Int -> Int -> Int
prim__shlChar : Char -> Char -> Char
prim__shlBigInt : Integer -> Integer -> Integer
prim__shlB8 : Bits8 -> Bits8 -> Bits8
prim__shlB64 : Bits64 -> Bits64 -> Bits64
prim__shlB32 : Bits32 -> Bits32 -> Bits32
prim__shlB16 : Bits16 -> Bits16 -> Bits16
prim__sgteInt : Int -> Int -> Int
prim__sgteFloat : Double -> Double -> Int
prim__sgteChar : Char -> Char -> Int
prim__sgteBigInt : Integer -> Integer -> Int
prim__sgteB8 : Bits8 -> Bits8 -> Int
prim__sgteB64 : Bits64 -> Bits64 -> Int
prim__sgteB32 : Bits32 -> Bits32 -> Int
prim__sgteB16 : Bits16 -> Bits16 -> Int
prim__sgtInt : Int -> Int -> Int
prim__sgtFloat : Double -> Double -> Int
prim__sgtChar : Char -> Char -> Int
prim__sgtBigInt : Integer -> Integer -> Int
prim__sgtB8 : Bits8 -> Bits8 -> Int
prim__sgtB64 : Bits64 -> Bits64 -> Int
prim__sgtB32 : Bits32 -> Bits32 -> Int
prim__sgtB16 : Bits16 -> Bits16 -> Int
prim__sextInt_BigInt : Int -> Integer
prim__sextInt_B64 : Int -> Bits64
prim__sextInt_B32 : Int -> Bits32
prim__sextInt_B16 : Int -> Bits16
prim__sextChar_BigInt : Char -> Integer
prim__sextB8_Int : Bits8 -> Int
prim__sextB8_BigInt : Bits8 -> Integer
prim__sextB8_B64 : Bits8 -> Bits64
prim__sextB8_B32 : Bits8 -> Bits32
prim__sextB8_B16 : Bits8 -> Bits16
prim__sextB64_BigInt : Bits64 -> Integer
prim__sextB32_Int : Bits32 -> Int
prim__sextB32_BigInt : Bits32 -> Integer
prim__sextB32_B64 : Bits32 -> Bits64
prim__sextB16_Int : Bits16 -> Int
prim__sextB16_BigInt : Bits16 -> Integer
prim__sextB16_B64 : Bits16 -> Bits64
prim__sextB16_B32 : Bits16 -> Bits32
prim__sdivInt : Int -> Int -> Int
prim__sdivChar : Char -> Char -> Char
prim__sdivBigInt : Integer -> Integer -> Integer
prim__sdivB8 : Bits8 -> Bits8 -> Bits8
prim__sdivB64 : Bits64 -> Bits64 -> Bits64
prim__sdivB32 : Bits32 -> Bits32 -> Bits32
prim__sdivB16 : Bits16 -> Bits16 -> Bits16
prim__registerPtr : Ptr -> Int -> ManagedPtr
prim__readString : prim__WorldType -> String
prim__readFile : prim__WorldType -> Ptr -> String
prim__ptrOffset : Ptr -> Int -> Ptr
prim__pokeSingle : prim__WorldType -> Ptr -> Int -> Double -> Int
prim__pokePtr : prim__WorldType -> Ptr -> Int -> Ptr -> Int
prim__pokeDouble : prim__WorldType -> Ptr -> Int -> Double -> Int
prim__poke8 : prim__WorldType -> Ptr -> Int -> Bits8 -> Int
prim__poke64 : prim__WorldType -> Ptr -> Int -> Bits64 -> Int
prim__poke32 : prim__WorldType -> Ptr -> Int -> Bits32 -> Int
prim__poke16 : prim__WorldType -> Ptr -> Int -> Bits16 -> Int
prim__peekSingle : prim__WorldType -> Ptr -> Int -> Double
prim__peekPtr : prim__WorldType -> Ptr -> Int -> Ptr
prim__peekDouble : prim__WorldType -> Ptr -> Int -> Double
prim__peek8 : prim__WorldType -> Ptr -> Int -> Bits8
prim__peek64 : prim__WorldType -> Ptr -> Int -> Bits64
prim__peek32 : prim__WorldType -> Ptr -> Int -> Bits32
prim__peek16 : prim__WorldType -> Ptr -> Int -> Bits16
prim__orInt : Int -> Int -> Int
prim__orChar : Char -> Char -> Char
prim__orBigInt : Integer -> Integer -> Integer
prim__orB8 : Bits8 -> Bits8 -> Bits8
prim__orB64 : Bits64 -> Bits64 -> Bits64
prim__orB32 : Bits32 -> Bits32 -> Bits32
prim__orB16 : Bits16 -> Bits16 -> Bits16
prim__null : Ptr
prim__negFloat : Double -> Double
prim__mulInt : Int -> Int -> Int
prim__mulFloat : Double -> Double -> Double
prim__mulChar : Char -> Char -> Char
prim__mulBigInt : Integer -> Integer -> Integer
prim__mulB8 : Bits8 -> Bits8 -> Bits8
prim__mulB64 : Bits64 -> Bits64 -> Bits64
prim__mulB32 : Bits32 -> Bits32 -> Bits32
prim__mulB16 : Bits16 -> Bits16 -> Bits16
prim__lteChar : Char -> Char -> Int
prim__lteBigInt : Integer -> Integer -> Int
prim__lteB8 : Bits8 -> Bits8 -> Int
prim__lteB64 : Bits64 -> Bits64 -> Int
prim__lteB32 : Bits32 -> Bits32 -> Int
prim__lteB16 : Bits16 -> Bits16 -> Int
prim__ltString : String -> String -> Int
prim__ltChar : Char -> Char -> Int
prim__ltBigInt : Integer -> Integer -> Int
prim__ltB8 : Bits8 -> Bits8 -> Int
prim__ltB64 : Bits64 -> Bits64 -> Int
prim__ltB32 : Bits32 -> Bits32 -> Int
prim__ltB16 : Bits16 -> Bits16 -> Int
prim__lshrInt : Int -> Int -> Int
prim__lshrChar : Char -> Char -> Char
prim__lshrBigInt : Integer -> Integer -> Integer
prim__lshrB8 : Bits8 -> Bits8 -> Bits8
prim__lshrB64 : Bits64 -> Bits64 -> Bits64
prim__lshrB32 : Bits32 -> Bits32 -> Bits32
prim__lshrB16 : Bits16 -> Bits16 -> Bits16
prim__intToChar : Int -> Char
prim__gteChar : Char -> Char -> Int
prim__gteBigInt : Integer -> Integer -> Int
prim__gteB8 : Bits8 -> Bits8 -> Int
prim__gteB64 : Bits64 -> Bits64 -> Int
prim__gteB32 : Bits32 -> Bits32 -> Int
prim__gteB16 : Bits16 -> Bits16 -> Int
prim__gtChar : Char -> Char -> Int
prim__gtBigInt : Integer -> Integer -> Int
prim__gtB8 : Bits8 -> Bits8 -> Int
prim__gtB64 : Bits64 -> Bits64 -> Int
prim__gtB32 : Bits32 -> Bits32 -> Int
prim__gtB16 : Bits16 -> Bits16 -> Int
prim__fromStrInt : String -> Int
prim__fromStrChar : String -> Char
prim__fromStrBigInt : String -> Integer
prim__fromStrB8 : String -> Bits8
prim__fromStrB64 : String -> Bits64
prim__fromStrB32 : String -> Bits32
prim__fromStrB16 : String -> Bits16
prim__fromFloatInt : Double -> Int
prim__fromFloatChar : Double -> Char
prim__fromFloatBigInt : Double -> Integer
prim__fromFloatB8 : Double -> Bits8
prim__fromFloatB64 : Double -> Bits64
prim__fromFloatB32 : Double -> Bits32
prim__fromFloatB16 : Double -> Bits16
prim__floatToStr : Double -> String
prim__floatTan : Double -> Double
prim__floatSqrt : Double -> Double
prim__floatSin : Double -> Double
prim__floatLog : Double -> Double
prim__floatFloor : Double -> Double
prim__floatExp : Double -> Double
prim__floatCos : Double -> Double
prim__floatCeil : Double -> Double
prim__floatATan : Double -> Double
prim__floatASin : Double -> Double
prim__floatACos : Double -> Double
prim__eqString : String -> String -> Int
prim__eqPtr : Ptr -> Ptr -> Int
prim__eqManagedPtr : ManagedPtr -> ManagedPtr -> Int
prim__eqInt : Int -> Int -> Int
prim__eqFloat : Double -> Double -> Int
prim__eqChar : Char -> Char -> Int
prim__eqBigInt : Integer -> Integer -> Int
prim__eqB8 : Bits8 -> Bits8 -> Int
prim__eqB64 : Bits64 -> Bits64 -> Int
prim__eqB32 : Bits32 -> Bits32 -> Int
prim__eqB16 : Bits16 -> Bits16 -> Int
prim__divFloat : Double -> Double -> Double
prim__concat : String -> String -> String
prim__complInt : Int -> Int
prim__complChar : Char -> Char
prim__complBigInt : Integer -> Integer
prim__complB8 : Bits8 -> Bits8
prim__complB64 : Bits64 -> Bits64
prim__complB32 : Bits32 -> Bits32
prim__complB16 : Bits16 -> Bits16
prim__charToInt : Char -> Int
prim__believe_me : (a : Type) -> (b : Type) -> (x : a) -> b
prim__ashrInt : Int -> Int -> Int
prim__ashrChar : Char -> Char -> Char
prim__ashrBigInt : Integer -> Integer -> Integer
prim__ashrB8 : Bits8 -> Bits8 -> Bits8
prim__ashrB64 : Bits64 -> Bits64 -> Bits64
prim__ashrB32 : Bits32 -> Bits32 -> Bits32
prim__ashrB16 : Bits16 -> Bits16 -> Bits16
prim__asPtr : ManagedPtr -> Ptr
prim__andInt : Int -> Int -> Int
prim__andChar : Char -> Char -> Char
prim__andBigInt : Integer -> Integer -> Integer
prim__andB8 : Bits8 -> Bits8 -> Bits8
prim__andB64 : Bits64 -> Bits64 -> Bits64
prim__andB32 : Bits32 -> Bits32 -> Bits32
prim__andB16 : Bits16 -> Bits16 -> Bits16
prim__addInt : Int -> Int -> Int
prim__addFloat : Double -> Double -> Double
prim__addChar : Char -> Char -> Char
prim__addBigInt : Integer -> Integer -> Integer
prim__addB8 : Bits8 -> Bits8 -> Bits8
prim__addB64 : Bits64 -> Bits64 -> Bits64
prim__addB32 : Bits32 -> Bits32 -> Bits32
prim__addB16 : Bits16 -> Bits16 -> Bits16
par : Lazy a -> a
mkForeignPrim : ForeignPrimType xs env t
liftPrimIO : (World -> PrimIO a) -> IO' l a
io_pure : a -> IO' l a
io_bind : IO' l a -> (a -> IO' l b) -> IO' l b
foreign : (f : FFI) -> (fname : ffi_fn f) -> (ty : Type) -> {auto fty : FTy f [] ty} -> ty

Call a foreign function.

The particular semantics of foreign function calls depend on the
Idris compiler backend in use. For the default C backend, see the
documentation for FFI_C.

For more details, please consult the Idris documentation.

f

an FFI descriptor, which is specific to the compiler backend.

fname

the name of the foreign function

ty

the Idris type for the foreign function

fty

an automatically-found proof that the Idris type works with
the FFI in question

call__IO : IO' ffi a -> PrimIO a
believe_me : a -> b

Subvert the type checker. This function is abstract, so it will not reduce in
the type checker. Use it with care - it can result in segfaults or worse!

assert_unreachable : a

Assert to the totality checker that the case using this expression
is unreachable

assert_total : a -> a

Assert to the totality checker that the given expression will always
terminate.

assert_smaller : (x : a) -> (y : b) -> b

Assert to the totality checker that y is always structurally smaller than
x (which is typically a pattern argument)

x

the larger value (typically a pattern argument)

y

the smaller value (typically an argument to a recursive call)

WorldRes : Type -> Type
data World : Type

A token representing the world, for use in IO

TheWorld : prim__WorldType -> World
data Void : Type

The empty type, also known as the trivially false proposition.

Use void or absurd to prove anything if you have a variable of type Void in scope.

data Unit : Type

The canonical single-element type, also known as the trivially
true proposition.

MkUnit : ()

The trivial constructor for ().

data Symbol_ : String -> Type

For 'symbol syntax. 'foo becomes Symbol_ "foo"

Ptr : Type
data PrimIO : Type -> Type

Idris's primitive IO, for building abstractions on top of

Prim__IO : a -> PrimIO a
PE_with block in with block in Decidable.Equality.Decidable.Equality.List a implementation of Decidable.Equality.DecEq, method decEq_57346f05 : (x : String) -> (xs : List String) -> (y : String) -> (p : (x = y) -> Void) -> (ys : List String) -> (warg : Dec (xs = ys)) -> Dec (x :: xs = y :: ys)
PE_with block in with block in Decidable.Equality.Decidable.Equality.List a implementation of Decidable.Equality.DecEq, method decEq_221af628 : (x : String) -> (xs : List String) -> (ys : List String) -> (warg : Dec (xs = ys)) -> Dec (x :: xs = x :: ys)
PE_with block in with block in Decidable.Equality.Decidable.Equality.(a, b) implementation of Decidable.Equality.DecEq, method decEq_429d3a44 : (a1 : Int) -> (a' : Int) -> (p : (a1 = a') -> Void) -> (b1 : Int) -> (b' : Int) -> (warg : Dec (b1 = b')) -> Dec ((a1, b1) = (a', b'))
PE_with block in with block in Decidable.Equality.Decidable.Equality.(a, b) implementation of Decidable.Equality.DecEq, method decEq_325588ab : (a1 : Int) -> (b1 : Int) -> (b' : Int) -> (warg : Dec (b1 = b')) -> Dec ((a1, b1) = (a1, b'))
PE_with block in Decidable.Equality.Decidable.Equality.List a implementation of Decidable.Equality.DecEq, method decEq_41c8e31f : (x : String) -> (xs : List String) -> (y : String) -> (warg : Dec (x = y)) -> (ys : List String) -> Dec (x :: xs = y :: ys)
PE_with block in Decidable.Equality.Decidable.Equality.(a, b) implementation of Decidable.Equality.DecEq, method decEq_e7d52819 : (a1 : Int) -> (a' : Int) -> (warg : Dec (a1 = a')) -> (b1 : Int) -> (b' : Int) -> Dec ((a1, b1) = (a', b'))
PE_uninhabited_82bd14b5 : Fin 0 -> Void
PE_toNat_99a6148 : Fin (S n) -> Nat
PE_toNat_4c658d6f : Int -> Nat
PE_toNat_127246ad : Char -> Nat
PE_succ_a550661c : Integer -> Integer
PE_succ_a521ac26 : Nat -> Nat
PE_succ_99a6148 : Fin (S n) -> Fin (S n)
PE_succ_4c658d6f : Int -> Int
PE_succ_127246ad : Char -> Char
PE_stateType, StateT stateType m implementation of Control.Monad.State.MonadState_e16c4eee : MonadState stateType (StateT stateType Identity)
PE_show_eb6946c9 : (x : Nat) -> String
PE_show_e7c136d6 : (x : Int) -> String
PE_show_b67bc069 : (x : Integer) -> String
PE_show_a0ccdda : (x : GameState) -> String
PE_quotedTy_ff94a715 : TT
PE_quotedTy_fa9e27bf : TT
PE_quotedTy_f9c892eb : Raw
PE_quotedTy_f4aa0711 : Raw
PE_quotedTy_e2e8cd5f : TT
PE_quotedTy_d93ebe1 : TT
PE_quotedTy_d6fa46de : Raw
PE_quotedTy_d1605ed3 : Raw
PE_quotedTy_cf6605b0 : TT
PE_quotedTy_cb592260 : TT
PE_quotedTy_c986b929 : Raw
PE_quotedTy_c6d2396b : Raw
PE_quotedTy_bad665b9 : Raw
PE_quotedTy_b59f201e : Raw
PE_quotedTy_b0b87011 : TT
PE_quotedTy_b0552d4e : Raw
PE_quotedTy_ae3f491e : TT
PE_quotedTy_ab40cb60 : TT
PE_quotedTy_a705dfab : TT
PE_quotedTy_a5cf0053 : TT
PE_quotedTy_a5b26176 : Raw
PE_quotedTy_9df05854 : Raw
PE_quotedTy_9b544316 : Raw
PE_quotedTy_97884f33 : Raw
PE_quotedTy_91928ce3 : TT
PE_quotedTy_8fec9e80 : Raw
PE_quotedTy_7e1bed6d : TT
PE_quotedTy_7c8cff33 : Raw
PE_quotedTy_60e0b958 : Raw
PE_quotedTy_5d1796a9 : TT
PE_quotedTy_5a9203f2 : TT
PE_quotedTy_5912c457 : TT
PE_quotedTy_51fc362d : Raw
PE_quotedTy_4f1d897d : Raw
PE_quotedTy_4bd465ad : TT
PE_quotedTy_4b1385cc : Raw
PE_quotedTy_47a744fe : TT
PE_quotedTy_4215c935 : TT
PE_quotedTy_3a22bdf0 : Raw
PE_quotedTy_35074306 : TT
PE_quotedTy_335d430c : TT
PE_quotedTy_32680f04 : Raw
PE_quotedTy_30c462d8 : Raw
PE_quotedTy_2ebe935f : TT
PE_quotedTy_2bfe0b32 : TT
PE_quotedTy_2b54d65f : Raw
PE_quotedTy_1de4abb0 : Raw
PE_quotedTy_11b0c7fc : TT
PE_quote_fb25be7e : Universe -> TT
PE_quote_f7929890 : Char -> Raw
PE_quote_f42cac99 : Bits8 -> Raw
PE_quote_f2e8b04b : Tactic -> TT
PE_quote_f166ba4a : Nat -> Raw
PE_quote_ec31e2d : Char -> TT
PE_quote_ea4ce2fa : Bits8 -> TT
PE_quote_e9df6dce : TTUExp -> TT
PE_quote_e2ed6f1b : NativeTy -> Raw
PE_quote_e2ce602 : FunArg -> Raw
PE_quote_e2a453a6 : ArithTy -> Raw
PE_quote_da7a21f4 : CtorArg -> Raw
PE_quote_d574f7da : List String -> TT
PE_quote_d0bb458c : Bits16 -> Raw
PE_quote_cc5019ba : Bits64 -> Raw
PE_quote_c6d67f16 : Integer -> TT
PE_quote_c3e429ae : (List CtorArg, Raw) -> TT
PE_quote_c011684a : TTName -> TT
PE_quote_bb2e64bb : Double -> Raw
PE_quote_bafad783 : Raw -> Raw
PE_quote_bad06abc : Const -> TT
PE_quote_b6432314 : (List CtorArg, Raw) -> Raw
PE_quote_acd28285 : List CtorArg -> TT
PE_quote_abbf71c1 : FunArg -> TT
PE_quote_a9687b81 : Double -> TT
PE_quote_a590cd43 : NameType -> TT
PE_quote_a202e3dc : Integer -> Raw
PE_quote_9f01864d : List TyConArg -> TT
PE_quote_9d1f6fb7 : TTUExp -> Raw
PE_quote_9814dcee : Bits32 -> Raw
PE_quote_94ccc80c : TT -> Raw
PE_quote_9182fc1a : TyConArg -> Raw
PE_quote_8ee1087 : Int -> TT
PE_quote_89eae9ab : ConstructorDefn -> Raw
PE_quote_890e238d : IntTy -> TT
PE_quote_87c378e8 : List ConstructorDefn -> Raw
PE_quote_84cef02f : ErrorReportPart -> TT
PE_quote_832c8b0a : List FunArg -> Raw
PE_quote_6e6f9378 : ArithTy -> TT
PE_quote_6d9a7cc4 : Bits16 -> TT
PE_quote_6b886a61 : Int -> Raw
PE_quote_699929e7 : NativeTy -> TT
PE_quote_69832452 : TTName -> Raw
PE_quote_690ff89 : CtorArg -> TT
PE_quote_65d83cd3 : Bits64 -> TT
PE_quote_64dd28b : List TyConArg -> Raw
PE_quote_63a43467 : NameType -> Raw
PE_quote_5bfb6346 : List CtorArg -> Raw
PE_quote_560bfa4 : Plicity -> TT
PE_quote_4f8acf73 : Universe -> Raw
PE_quote_4e63200b : String -> TT
PE_quote_4d45473c : Const -> Raw
PE_quote_490ee881 : Plicity -> Raw
PE_quote_47c9c7c2 : ConstructorDefn -> TT
PE_quote_43e1bb39 : TT -> TT
PE_quote_43132ca3 : Nat -> TT
PE_quote_3ea57e72 : List ErrorReportPart -> TT
PE_quote_3e6444b7 : Erasure -> TT
PE_quote_3c8fe520 : Raw -> TT
PE_quote_3b3a2889 : SourceLocation -> TT
PE_quote_386504a4 : Bits32 -> TT
PE_quote_36b7fc6a : IntTy -> Raw
PE_quote_367d6ed3 : TyConArg -> TT
PE_quote_362ee2f3 : List ConstructorDefn -> TT
PE_quote_32ceb976 : ErrorReportPart -> Raw
PE_quote_2df8d19d : Erasure -> Raw
PE_quote_1c19d025 : List String -> Raw
PE_quote_1af092e8 : List ErrorReportPart -> Raw
PE_quote_18691d0d : List FunArg -> TT
PE_quote_16b4e4fa : SourceLocation -> Raw
PE_quote_15a31d43 : String -> Raw
PE_quote_10f38c58 : Tactic -> Raw
PE_pure_7269de45 : a -> Elab a
PE_pure_4095ad26 : a -> IO' ffi a
PE_pack_16311912 : List Char -> String
PE_neutral_a2d785 : List a
PE_neutral_1aa80e66 : List b
PE_negate_a0372e3d : Int -> Int
PE_negate_888348d9 : Integer -> Integer
PE_negate_1438faaf : Double -> Double
PE_mod_144d4233 : Integer -> Integer -> Integer
PE_map_fda199ac : (func : a -> b) -> Stream a -> Stream b
PE_map_e5a2be8d : (func : a -> b) -> Elab a -> Elab b
PE_map_a8140cc3 : (func : a -> b) -> List a -> List b
PE_map_9090a046 : (func : a -> b) -> Identity a -> Identity b
PE_map_70be917a : (func : a -> b) -> Maybe a -> Maybe b
PE_map_1615b5d9 : (func : a -> b) -> Vect k a -> Vect k b
PE_isSuffixOf_51064304 : List Char -> List Char -> Bool
PE_isPrefixOf_51064304 : List Char -> List Char -> Bool
PE_isInfixOf_51064304 : List Char -> List Char -> Bool
PE_fromNat_4c658d6f : Nat -> Int
PE_fromNat_127246ad : Nat -> Char
PE_fromInteger_cefde01 : Integer -> Bits32
PE_fromInteger_aee05fe0 : Integer -> Nat
PE_fromInteger_a0377313 : Integer -> Int
PE_fromInteger_91a4ad2 : Integer -> Bits16
PE_fromInteger_88838daf : Integer -> Integer
PE_fromInteger_44bb4583 : Integer -> Bits64
PE_fromInteger_39f8582d : Integer -> Bits8
PE_fromInteger_14393f85 : Integer -> Double
PE_foldr_b9bf48b9 : (func : elem -> acc -> acc) -> (init : acc) -> (input : Vect n elem) -> acc
PE_foldr_b20bef9e : (func : elem -> acc -> acc) -> (init : acc) -> (input : Binder elem) -> acc
PE_foldr_8c919c47 : (func : elem -> acc -> acc) -> (init : acc) -> (input : List elem) -> acc
PE_foldr_16f7eded : (func : elem -> acc -> acc) -> (init : acc) -> (input : List elem) -> acc
PE_foldr_15b4eacd : (func : elem -> acc -> acc) -> (init : acc) -> (input : Maybe elem) -> acc
PE_foldl_8c919c47 : (func : acc -> elem -> acc) -> (init : acc) -> (input : List elem) -> acc
PE_foldl_16f7eded : (func : acc -> elem -> acc) -> (init : acc) -> (input : List elem) -> acc
PE_enumFrom_a550661c : Integer -> Stream Integer
PE_enumFrom_a521ac26 : Nat -> Stream Nat
PE_enumFrom_99a6148 : Fin (S n) -> Stream (Fin (S n))
PE_enumFrom_4c658d6f : Int -> Stream Int
PE_enumFrom_127246ad : Char -> Stream Char
PE_enumFromThen_d9173b9b : Int -> Int -> Stream Int
PE_enumFromThen_4f5d2a05 : Integer -> Integer -> Stream Integer
PE_elem_51064304 : Char -> List Char -> Bool
PE_div_cf294ead : Int -> Int -> Int
PE_div_144d4233 : Integer -> Integer -> Integer
PE_decEq_f7d1037b : (x1 : Int) -> (x2 : Int) -> Dec (x1 = x2)
PE_decEq_f472a916 : (x1 : Nat) -> (x2 : Nat) -> Dec (x1 = x2)
PE_decEq_b00edb69 : (x1 : String) -> (x2 : String) -> Dec (x1 = x2)
PE_decEq_ae236ae3 : (x1 : Bool) -> (x2 : Bool) -> Dec (x1 = x2)
PE_decEq_a773de4 : (x1 : (Int, Int)) -> (x2 : (Int, Int)) -> Dec (x1 = x2)
PE_decEq_2af79e3e : (x1 : SourceLocation) -> (x2 : SourceLocation) -> Dec (x1 = x2)
PE_decEq_2a06b3c8 : (x1 : Fin k) -> (x2 : Fin k) -> Dec (x1 = x2)
PE_decEq_18cc2957 : (x1 : List String) -> (x2 : List String) -> Dec (x1 = x2)
PE_constructor of Prelude.Monad.Monad#Applicative m_5cb6785b : Applicative Identity
PE_constructor of Prelude.Algebra.Monoid#Semigroup ty_a2d785 : Semigroup (List a)
PE_constructor of Prelude.Algebra.Monoid#Semigroup ty_1aa80e66 : Semigroup (List b)
PE_concat_a11e8ee1 : List (List a) -> List a
PE_concatMap_994c4fbe : (a -> List b) -> List a -> List b
PE_compare_b1f9e5e3 : String -> String -> Ordering
PE_compare_a73622eb : Int -> Int -> Ordering
PE_compare_9b717d84 : Double -> Double -> Ordering
PE_compare_9afb5b35 : () -> () -> Ordering
PE_compare_99059107 : Integer -> Integer -> Ordering
PE_compare_8afca964 : Nat -> Nat -> Ordering
PE_compare_79237e6e : Prec -> Prec -> Ordering
PE_compare_72843a86 : Char -> Char -> Ordering
PE_compare_6c7fdee8 : Bool -> Bool -> Ordering
PE_compare_457648e4 : Fin k -> Fin k -> Ordering
PE_cast_fec939d8 : (orig : String) -> Integer
PE_cast_e6ee2664 : (orig : Int) -> Integer
PE_cast_c68c9957 : (orig : Int) -> Char
PE_cast_9b787908 : (orig : String) -> List Char
PE_cast_8d4597ff : (orig : Nat) -> Integer
PE_cast_8ce94d78 : (orig : Nat) -> Int
PE_cast_8367c60 : (orig : Integer) -> Nat
PE_cast_58e3c687 : (orig : Char) -> Int
PE_cast_264fce1b : (orig : Int) -> Nat
PE_cast_14279f49 : (orig : String) -> Int
PE_any_db8074ec : (a -> Bool) -> List a -> Bool
PE_any_7258c85e : (a -> Bool) -> List a -> Bool
PE_all_7258c85e : (a -> Bool) -> List a -> Bool
PE_absurd_afbd316f : (h : Fin 0) -> a
PE_absurd_a4e54404 : (h : LTE (S spec) 0) -> a
PE_absurd_59df558d : (h : LTE (S n') 0) -> a
PE_abs_a0372e3d : Int -> Int
PE_abs_888348d9 : Integer -> Integer
PE_StateT stateType m implementation of Prelude.Monad.Monad_fcf656f6 : Monad (StateT stateType Identity)
PE_StateT stateType m implementation of Prelude.Monad.Monad_e16c4eee : Monad (StateT stateType Identity)
PE_StateT stateType f implementation of Prelude.Functor.Functor_8904f957 : Functor (StateT stateType Identity)
PE_StateT stateType f implementation of Prelude.Applicative.Applicative_fcf656f6 : Applicative (StateT stateType Identity)
PE_StateT stateType f implementation of Prelude.Applicative.Applicative_e16c4eee : Applicative (StateT stateType Identity)
PE_List a, TT implementation of Language.Reflection.Quotable_d7f1b1e8 : Quotable (List (TTName, List CtorArg, Raw)) TT
PE_List a, TT implementation of Language.Reflection.Quotable_c1cc936b : Quotable (List CtorArg) TT
PE_List a, TT implementation of Language.Reflection.Quotable_7b4b62bf : Quotable (List TyConArg) TT
PE_List a, TT implementation of Language.Reflection.Quotable_7b292525 : Quotable (List ConstructorDefn) TT
PE_List a, TT implementation of Language.Reflection.Quotable_798b5893 : Quotable (List FunArg) TT
PE_List a, TT implementation of Language.Reflection.Quotable_44052c46 : Quotable (List String) TT
PE_List a, TT implementation of Language.Reflection.Quotable_422f02c4 : Quotable (List ErrorReportPart) TT
PE_List a, Raw implementation of Language.Reflection.Quotable_fef4f8a9 : Quotable (List CtorArg) Raw
PE_List a, Raw implementation of Language.Reflection.Quotable_e84db271 : Quotable (List TyConArg) Raw
PE_List a, Raw implementation of Language.Reflection.Quotable_e3e3c1a0 : Quotable (List ConstructorDefn) Raw
PE_List a, Raw implementation of Language.Reflection.Quotable_c840ace5 : Quotable (List String) Raw
PE_List a, Raw implementation of Language.Reflection.Quotable_ae8c62d7 : Quotable (List FunArg) Raw
PE_List a, Raw implementation of Language.Reflection.Quotable_8ba55317 : Quotable (List ErrorReportPart) Raw
PE_List a, Raw implementation of Language.Reflection.Quotable_1c45f7a8 : Quotable (List (TTName, List CtorArg, Raw)) Raw
PE_List a implementation of Decidable.Equality.DecEq_2898581c : DecEq (List String)
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quotedTy_f8f9efbe : TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quotedTy_c1cc936b : TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quotedTy_932972bc : TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quotedTy_62fb8614 : TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quotedTy_3fc7d9d7 : TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quotedTy_389a58 : TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quotedTy_20e85888 : TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quotedTy_116b91 : TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_fb5f0128 : List CtorArg -> TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_f857caa5 : List ConstructorDefn -> TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_e4b7baef : List TyConArg -> TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_e04dca1e : List ConstructorDefn -> TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_c4aab564 : List String -> TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_c26c48eb : List ErrorReportPart -> TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_aaf66b56 : List FunArg -> TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_880f5b95 : List ErrorReportPart -> TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_3df369d0 : List TyConArg -> TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_38c31502 : List CtorArg -> TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_23ede0e : List String -> TT
PE_Language.Reflection.List a, TT implementation of Language.Reflection.Quotable, method quote_1837e7f9 : List FunArg -> TT
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quotedTy_fef4f8a9 : Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quotedTy_a079fb9f : Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quotedTy_98487701 : Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quotedTy_86612cc3 : Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quotedTy_80381f5d : Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quotedTy_7d8b9c5e : Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quotedTy_1c85508b : Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quotedTy_18434697 : Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_f20400f0 : List TyConArg -> Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_dd940e42 : List CtorArg -> Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_d05649f3 : List String -> Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_afb96fe1 : List ErrorReportPart -> Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_ad2f6248 : List ConstructorDefn -> Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_a1575783 : List TyConArg -> Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_873c0b53 : List CtorArg -> Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_8018be2a : List FunArg -> Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_605bf60c : List ConstructorDefn -> Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_4fb648 : List ErrorReportPart -> Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_2eff286d : List FunArg -> Raw
PE_Language.Reflection.List a, Raw implementation of Language.Reflection.Quotable, method quote_20ac19d1 : List String -> Raw
PE_Language.Reflection.(a, b), TT implementation of Language.Reflection.Quotable, method quotedTy_e2e051bb : TT
PE_Language.Reflection.(a, b), TT implementation of Language.Reflection.Quotable, method quotedTy_c897e3a8 : TT
PE_Language.Reflection.(a, b), TT implementation of Language.Reflection.Quotable, method quotedTy_aa8c6712 : TT
PE_Language.Reflection.(a, b), TT implementation of Language.Reflection.Quotable, method quotedTy_a633d2b4 : TT
PE_Language.Reflection.(a, b), TT implementation of Language.Reflection.Quotable, method quotedTy_69d2094d : TT
PE_Language.Reflection.(a, b), TT implementation of Language.Reflection.Quotable, method quotedTy_6382b95c : TT
PE_Language.Reflection.(a, b), TT implementation of Language.Reflection.Quotable, method quotedTy_501f7f23 : TT
PE_Language.Reflection.(a, b), TT implementation of Language.Reflection.Quotable, method quote_fc1949ae : (TTName, List CtorArg, Raw) -> TT
PE_Language.Reflection.(a, b), TT implementation of Language.Reflection.Quotable, method quote_db94590e : (List CtorArg, Raw) -> TT
PE_Language.Reflection.(a, b), TT implementation of Language.Reflection.Quotable, method quote_d3d9e546 : (TTName, List CtorArg, Raw) -> TT
PE_Language.Reflection.(a, b), TT implementation of Language.Reflection.Quotable, method quote_a4133359 : (List CtorArg, Raw) -> TT
PE_Language.Reflection.(a, b), TT implementation of Language.Reflection.Quotable, method quote_6cae29a4 : (List CtorArg, Raw) -> TT
PE_Language.Reflection.(a, b), TT implementation of Language.Reflection.Quotable, method quote_540f63d9 : (TTName, List CtorArg, Raw) -> TT
PE_Language.Reflection.(a, b), TT implementation of Language.Reflection.Quotable, method quote_3eea8986 : (List CtorArg, Raw) -> TT
PE_Language.Reflection.(a, b), Raw implementation of Language.Reflection.Quotable, method quotedTy_f744bf2e : Raw
PE_Language.Reflection.(a, b), Raw implementation of Language.Reflection.Quotable, method quotedTy_d9b9567c : Raw
PE_Language.Reflection.(a, b), Raw implementation of Language.Reflection.Quotable, method quotedTy_c5c91370 : Raw
PE_Language.Reflection.(a, b), Raw implementation of Language.Reflection.Quotable, method quotedTy_b4e26040 : Raw
PE_Language.Reflection.(a, b), Raw implementation of Language.Reflection.Quotable, method quotedTy_90b130e : Raw
PE_Language.Reflection.(a, b), Raw implementation of Language.Reflection.Quotable, method quotedTy_8a1aecb8 : Raw
PE_Language.Reflection.(a, b), Raw implementation of Language.Reflection.Quotable, method quotedTy_69ea998a : Raw
PE_Language.Reflection.(a, b), Raw implementation of Language.Reflection.Quotable, method quote_dfdca563 : (TTName, List CtorArg, Raw) -> Raw
PE_Language.Reflection.(a, b), Raw implementation of Language.Reflection.Quotable, method quote_cd788413 : (List CtorArg, Raw) -> Raw
PE_Language.Reflection.(a, b), Raw implementation of Language.Reflection.Quotable, method quote_a73dcb1b : (TTName, List CtorArg, Raw) -> Raw
PE_Language.Reflection.(a, b), Raw implementation of Language.Reflection.Quotable, method quote_7eeb81da : (List CtorArg, Raw) -> Raw
PE_Language.Reflection.(a, b), Raw implementation of Language.Reflection.Quotable, method quote_512e68a6 : (List CtorArg, Raw) -> Raw
PE_Language.Reflection.(a, b), Raw implementation of Language.Reflection.Quotable, method quote_2a6d7520 : (List CtorArg, Raw) -> Raw
PE_Language.Reflection.(a, b), Raw implementation of Language.Reflection.Quotable, method quote_10e42674 : (TTName, List CtorArg, Raw) -> Raw
PE_Decidable.Equality.List a implementation of Decidable.Equality.DecEq, method decEq_b00edb69 : (x1 : List String) -> (x2 : List String) -> Dec (x1 = x2)
PE_Decidable.Equality.List a implementation of Decidable.Equality.DecEq, method decEq_2c46616 : (x1 : List String) -> (x2 : List String) -> Dec (x1 = x2)
PE_Decidable.Equality.(a, b) implementation of Decidable.Equality.DecEq, method decEq_b7544297 : (x1 : (Int, Int)) -> (x2 : (Int, Int)) -> Dec (x1 = x2)
PE_Decidable.Equality.(a, b) implementation of Decidable.Equality.DecEq, method decEq_40230390 : (x1 : (Int, Int)) -> (x2 : (Int, Int)) -> Dec (x1 = x2)
PE_Control.Monad.State.stateType, StateT stateType m implementation of Control.Monad.State.MonadState, method put_c138374 : stateType -> StateT stateType Identity ()
PE_Control.Monad.State.stateType, StateT stateType m implementation of Control.Monad.State.MonadState, method get_843ea6e2 : StateT stateType Identity stateType
PE_Control.Monad.State.StateT stateType m implementation of Prelude.Monad.Monad, method join_c60f2043 : StateT stateType Identity (StateT stateType Identity a) -> StateT stateType Identity a
PE_Control.Monad.State.StateT stateType m implementation of Prelude.Monad.Monad, method >>=_af49394a : StateT stateType Identity a -> (a -> StateT stateType Identity b) -> StateT stateType Identity b
PE_Control.Monad.State.StateT stateType f implementation of Prelude.Functor.Functor, method map_b1448166 : (func : a -> b) -> StateT stateType Identity a -> StateT stateType Identity b
PE_Control.Monad.State.StateT stateType f implementation of Prelude.Applicative.Applicative, method pure_c60f2043 : a -> StateT stateType Identity a
PE_Control.Monad.State.StateT stateType f implementation of Prelude.Applicative.Applicative, method <*>_af49394a : StateT stateType Identity (a -> b) -> StateT stateType Identity a -> StateT stateType Identity b
PE_>_fed9e9de : Fin n -> Fin n -> Bool
PE_>_dc344345 : Bits64 -> Bits64 -> Bool
PE_>_b1f9e5e3 : String -> String -> Bool
PE_>_aafbeb83 : Bits32 -> Bits32 -> Bool
PE_>_a73622eb : Int -> Int -> Bool
PE_>_9b717d84 : Double -> Double -> Bool
PE_>_9afb5b35 : () -> () -> Bool
PE_>_99059107 : Integer -> Integer -> Bool
PE_>_8afca964 : Nat -> Nat -> Bool
PE_>_79237e6e : Prec -> Prec -> Bool
PE_>_7913ab39 : Bits8 -> Bits8 -> Bool
PE_>_72843a86 : Char -> Char -> Bool
PE_>_6c7fdee8 : Bool -> Bool -> Bool
PE_>_2c73f279 : Bits16 -> Bits16 -> Bool
PE_>>=_d517bc2 : Elab a -> (a -> Elab b) -> Elab b
PE_>>=_d476d812 : Identity a -> (a -> Identity b) -> Identity b
PE_>>=_9eadab1d : Maybe a -> (a -> Maybe b) -> Maybe b
PE_>>=_8367c42a : List a -> (a -> List b) -> List b
PE_>>=_71aaca08 : Either e a -> (a -> Either e b) -> Either e b
PE_>>=_6cf29f6d : IO' ffi a -> (a -> IO' ffi b) -> IO' ffi b
PE_>>=_65adef24 : StateT stateType Identity a -> (a -> StateT stateType Identity b) -> StateT stateType Identity b
PE_>>=_59a46e47 : PrimIO a -> (a -> PrimIO b) -> PrimIO b
PE_>>=_3dd459a3 : Provider a -> (a -> Provider b) -> Provider b
PE_>>=_2c09df5e : Stream a -> (a -> Stream b) -> Stream b
PE_>>=_25fb8f9f : Vect n a -> (a -> Vect n b) -> Vect n b
PE_>=_a73622eb : Int -> Int -> Bool
PE_>=_99059107 : Integer -> Integer -> Bool
PE_>=_79237e6e : Prec -> Prec -> Bool
PE_>=_72843a86 : Char -> Char -> Bool
PE_==_feff0ea3 : Ordering -> Ordering -> Bool
PE_==_e0b15c81 : Ptr -> Ptr -> Bool
PE_==_d62124f9 : () -> () -> Bool
PE_==_ceadbc6 : Bits32 -> Bits32 -> Bool
PE_==_bdc90bbe : Fin k -> Fin k -> Bool
PE_==_b5b0cbe0 : Bool -> Bool -> Bool
PE_==_aedb5da5 : Nat -> Nat -> Bool
PE_==_a03270d8 : Int -> Int -> Bool
PE_==_9154897 : Bits16 -> Bits16 -> Bool
PE_==_910211e7 : String -> String -> Bool
PE_==_887e8b74 : Integer -> Integer -> Bool
PE_==_6ec5564b : ManagedPtr -> ManagedPtr -> Bool
PE_==_51064304 : Char -> Char -> Bool
PE_==_44b64348 : Bits64 -> Bits64 -> Bool
PE_==_39f3d0b6 : Prec -> Prec -> Bool
PE_==_39f355f2 : Bits8 -> Bits8 -> Bool
PE_==_14343d4a : Double -> Double -> Bool
PE_<_fed9e9de : Fin n -> Fin n -> Bool
PE_<_dc344345 : Bits64 -> Bits64 -> Bool
PE_<_b1f9e5e3 : String -> String -> Bool
PE_<_aafbeb83 : Bits32 -> Bits32 -> Bool
PE_<_a73622eb : Int -> Int -> Bool
PE_<_9b717d84 : Double -> Double -> Bool
PE_<_9afb5b35 : () -> () -> Bool
PE_<_99059107 : Integer -> Integer -> Bool
PE_<_8afca964 : Nat -> Nat -> Bool
PE_<_79237e6e : Prec -> Prec -> Bool
PE_<_7913ab39 : Bits8 -> Bits8 -> Bool
PE_<_72843a86 : Char -> Char -> Bool
PE_<_6c7fdee8 : Bool -> Bool -> Bool
PE_<_2c73f279 : Bits16 -> Bits16 -> Bool
PE_<=_a73622eb : Int -> Int -> Bool
PE_<=_99059107 : Integer -> Integer -> Bool
PE_<=_8afca964 : Nat -> Nat -> Bool
PE_<=_72843a86 : Char -> Char -> Bool
PE_<$>_dfea8e8c : (func : a -> b) -> Elab a -> Elab b
PE_/_6c6ee831 : Double -> Double -> Double
PE_/=_a03270d8 : Int -> Int -> Bool
PE_-_a71cf640 : Int -> Int -> Int
PE_-_9b5850d9 : Double -> Double -> Double
PE_-_98ec645c : Integer -> Integer -> Integer
PE_+_a725d5d6 : Int -> Int -> Int
PE_+_9b61306f : Double -> Double -> Double
PE_+_98f543f2 : Integer -> Integer -> Integer
PE_+_8aec5c4f : Nat -> Nat -> Nat
PE_*_a725d5d6 : Int -> Int -> Int
PE_*_98f543f2 : Integer -> Integer -> Integer
PE_*_8aec5c4f : Nat -> Nat -> Nat
PE_(a, b), TT implementation of Language.Reflection.Quotable_e19a8e6 : Quotable (List CtorArg, Raw) TT
PE_(a, b), TT implementation of Language.Reflection.Quotable_ab72a78f : Quotable (TTName, List CtorArg, Raw) TT
PE_(a, b), TT implementation of Language.Reflection.Quotable_1453872e : Quotable (TTName, List CtorArg, Raw) TT
PE_(a, b), Raw implementation of Language.Reflection.Quotable_bb8d470e : Quotable (TTName, List CtorArg, Raw) Raw
PE_(a, b), Raw implementation of Language.Reflection.Quotable_4bcb8aed : Quotable (TTName, List CtorArg, Raw) Raw
PE_(a, b), Raw implementation of Language.Reflection.Quotable_2ebe42b : Quotable (List CtorArg, Raw) Raw
PE_(a, b) implementation of Decidable.Equality.DecEq_d10b14ad : DecEq (Int, Int)
MkFFI : (ffi_types : Type -> Type) -> (ffi_fn : Type) -> (ffi_data : Type) -> FFI
ffi_types

A family describing which types are available in the FFI

ffi_fn

The type used to specify the names of foreign functions in this FFI

ffi_data

How this FFI describes exported datatypes

ManagedPtr : Type
Lazy : Type -> Type

Lazily evaluated values.
At run time, the delayed value will only be computed when required by
a case split.

data JsFn : Type -> Type
MkJsFn : (x : t) -> JsFn t
data JS_Types : Type -> Type
JS_Str : JS_Types String
JS_Float : JS_Types Double
JS_Ptr : JS_Types Ptr
JS_Unit : JS_Types ()
JS_FnT : JS_FnTypes a -> JS_Types (JsFn a)
JS_IntT : JS_IntTypes i -> JS_Types i
data JS_IntTypes : Type -> Type
JS_IntChar : JS_IntTypes Char
JS_IntNative : JS_IntTypes Int
JS_IO : Type -> Type
data JS_FnTypes : Type -> Type
JS_Fn : JS_Types s -> JS_FnTypes t -> JS_FnTypes (s -> t)
JS_FnIO : JS_Types t -> JS_FnTypes (IO' l t)
JS_FnBase : JS_Types t -> JS_FnTypes t
Inf : Type -> Type

Possibly infinite data.
A value which may be infinite is accepted by the totality checker if
it appears under a data constructor. At run time, the delayed value will
only be computed when required by a case split.

data IO' : (lang : FFI) -> Type -> Type

The IO type, parameterised over the FFI that is available within
it.

MkIO : (World -> PrimIO (WorldRes a)) -> IO' lang a
IO : (res : Type) -> Type

Interactive programs, describing I/O actions and returning a value.

res

The result type of the program

ForeignPrimType : (xs : List Type) -> FEnv ffi xs -> Type -> Type
Force : Delayed t a -> a

Compute a value from a delayed computation.

Inserted by the elaborator where necessary.

Float : Type

Deprecated alias for Double, for the purpose of backwards
compatibility. Idris does not support 32 bit floats at present.

data FTy : FFI -> List Type -> Type -> Type
FRet : ffi_types f t -> FTy f xs (IO' f t)
FFun : ffi_types f s -> FTy f (s :: xs) t -> FTy f xs (s -> t)
FFI_JS : FFI

The JavaScript FFI. The strings naming functions in this API are
JavaScript code snippets, into which the arguments are substituted
for the placeholders %0, %1, etc.

record FFI 

An FFI specifier, which describes how a particular compiler
backend handles foreign function calls.

MkFFI : (ffi_types : Type -> Type) -> (ffi_fn : Type) -> (ffi_data : Type) -> FFI
ffi_types

A family describing which types are available in the FFI

ffi_fn

The type used to specify the names of foreign functions in this FFI

ffi_data

How this FFI describes exported datatypes

ffi_types : (rec : FFI) -> Type -> Type

A family describing which types are available in the FFI

ffi_fn : (rec : FFI) -> Type

The type used to specify the names of foreign functions in this FFI

ffi_data : (rec : FFI) -> Type

How this FFI describes exported datatypes

data Delayed : DelayReason -> Type -> Type

The underlying implementation of Lazy and Inf.

Delay : (val : a) -> Delayed t a

A delayed computation.

Delay is inserted automatically by the elaborator where necessary.

Note that compiled code gives Delay special semantics.

t

whether this is laziness from an infinite structure or lazy evaluation

a

the type of the eventual value

val

a computation that will produce a value

data DelayReason : Type

Two types of delayed computation: that arising from lazy functions, and that
arising from infinite data. They differ in their totality condition.

Infinite : DelayReason
LazyValue : DelayReason
CData : Type
data (=) : (x : A) -> (y : B) -> Type

The propositional equality type. A proof that x = y.

To use such a proof, pattern-match on it, and the two equal things will then need to be the same pattern.

Note: Idris's equality type is potentially heterogeneous, which means that it is possible to state equalities between values of potentially different types. However, Idris will attempt the homogeneous case unless it fails to typecheck.

You may need to use (~=~) to explicitly request heterogeneous equality.

A

the type of the left side of the equality

B

the type of the right side of the equality

Refl : x = x

A proof that x in fact equals x. To construct this, you must have already shown that both sides are in fact equal.

A

the type at which the equality is proven

x

the element shown to be equal to itself.